Section: Partnerships and Cooperations

International Initiatives

Visits of International Scientists

Long-term visitors

• Jean-Jacques Lévy (INRIA, France), director of the MSR-INRIA Joint Center, visited Formes from September 26 to November 18, gave lectures on reductions and causality.

• Pierre-Louis Curien (PPS, CNRS and University Paris 7) visited Formes in April and May, and co-organized a working group on rewriting theory and algebra.

• Joseph Sifakis (VERIMAG, France) visited Formes in March and October and participated to various working groups.

Short-term visitors

• Zhang Min (JAIST, Japan) gave a talk on December 20 on algebraic-based verification of a dynamic software updating system.

• Vladimir Voevodsky (IAS Princeton, USA), Fields Medal 2002, gave a talk on December 12 on univalent semantics of constructive type theories.

• Jianhua Gao (ISCAS, China) gave a talk on November 25 on the clausal presentation of theories in deduction modulo.

• Iddo Tzameret (ITCS, Tsinghua University) gave a talk on November 18 on short propositional refutations for dense random 3-CNF formulas.

• Eric Madelaine (INRIA, France) gave a talk on November 11 at Shenzhen SIAT on specification, model generation and verification of distributed applications.

• Jean-Raymond Abrial (ETH, Switzerland) gave a talk on September 9 on modeling, refining and proving with Event-B.

• Graham Steel (LSV, ENS Cachan, France) gave lectures on the security of APIs at Tsinghua University and Nokia from August 22 to August 25.

• Thomas Anberree (Nottingham University at Ningbo, China) gave a talk on June 22 on definable quotients in type theory.

• Hsu-Chun Yen (National Taiwan University) gave a talk on May 20 on two-way transducers and parametrized machines.

• Lijun Zhang (Denmark Technical University) gave a talk on May 13 on ODEs in probabilistic model checking.

• Flemming Nielson (Denmark Technical University) gave a talk on May 13 on model checking as static analysis of modal logic.

• Christian Urban (TU Munich, Germany) gave a talk on April 29 on verifying a regular expression matcher and formal language theory.

• Zhaohui Luo (University of London, UK) visited Formes in April and gave lectures on type theory from April 13 to April 19.

• On April 11, for the 1st Tsinghua Software Day organized by the Formes team, we had the following talks: A journey into the semantics of programming languages, by Pierre-Louis Curien; type theory and its application, by Zhaohui Luo; advances towards the formal proof of the classification of finite groups, by Georges Gonthier; from boolean to quantitative theories of software, by Tom Henzinger.

• Joseph Sifakis (VERIMAG, France) gave a talk on March 10 on a vision for computer science: the system perspective.

Participation In International Programs

• SIVES(http://formes.asia/cms/sives ) is a French-Chinese ANR-NSFC project for 2009-2011 between INRIA Formes , Tsinghua University and ST Microelectronics on the development of a “SImulation and Verification based platform for Embedded Systems” (coordinated by Frédéric Blanqui on the French side and Ming Gu on the Chinese side).

• Logical Frameworks is a grant from the National Science Foundation of China obtained by Jean-Pierre Jouannaud and Jianqi Li to sustain their work on the subject.